The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(O(1), O(n^1)).

(0) Obligation:

Runtime Complexity TRS:
The TRS R consists of the following rules:

a(b(a(x1))) → b(c(x1))
b(b(b(x1))) → c(b(x1))
c(x1) → a(b(x1))
c(d(x1)) → d(c(b(a(x1))))

Rewrite Strategy: INNERMOST

(1) CpxTrsMatchBoundsProof (EQUIVALENT transformation)

A linear upper bound on the runtime complexity of the TRS R could be shown with a Match Bound [MATCHBOUNDS1,MATCHBOUNDS2] of 2.
The certificate found is represented by the following graph.

Start state: 535
Accept states: [536, 537, 538]
Transitions:
535→536[a_1|0]
535→537[b_1|0]
535→538[c_1|0]
535→535[d_1|0]
535→539[b_1|1]
535→540[a_1|1]
539→538[a_1|1]
540→541[b_1|1]
541→542[c_1|1]
541→543[b_1|2]
542→538[d_1|1]
543→542[a_1|2]

(2) BOUNDS(O(1), O(n^1))